l:IdLnk, dt:tg:Id fp Type, tg:Id. rcv(l,tg)  dom(lnk-decl(l;dt)) ~ tg  dom(dt) 

latex

Definitions	deq-member(eq;x;L), , t  T, {T}, P  Q, x:A. B(x), SQType(T), x  dom(f), lnk-decl(l;dt), a:A fp B(a), IdLnk, Id, x. t(x), P & Q, x:A. B(x), (x  l), Knd, rcv(l,tg), P  Q, P  Q, map(f;as), KindDeq, IdDeq, b, Prop
Lemmas	l member wf, rcv one one, Id sq, iff imp equal bool, assert wf, deq-member wf, assert-deq-member, id-deq wf, Kind-deq wf, map wf, member map, Knd wf, rcv wf, fpf wf, Id wf, IdLnk wf, bool sq